$\forall$$T$:Type, ${\it as}$:($T$ List), $n$:\{0$\ldots\,\parallel$${\it as}$$\parallel$\}, $i$:\{0..($\parallel$${\it as}$$\parallel$ {-} $n$)$^{-}$\}.
\\[0ex]nth\_tl($n$;${\it as}$)[$i$] = ${\it as}$[($i$+$n$)] $\in$ $T$